es:ES, p:(E(E + Top)).
causal-predecessor(es;p)
 (a, b, c:E. same-thread(es;p;a;b)  same-thread(es;p;b;c)  same-thread(es;p;a;c)) 

latex

Definitions	causal-predecessor(es;p), x:AB(x), E, left + right, Top, t  T, ES, x:A. B(x), P  Q, same-thread(es;p;e;e')
Lemmas	causal-pred-wellfounded, event system wf, top wf, es-E wf, causal-predecessor wf, same-thread wf